/*
 * Promela representation of a modified version
 * of the problem in an attempt to verify
 * our property psi for the readers local counter
 * that the reader relies upon to deduce a correct
 * read value
 */

#define N 4
#define READERS 1
#define MAX_INCS 10000

int shared_counter[2*N];

inline inc_locally(num) {
	d_step {
		if
			:: num == MAX_INCS;
			skip;
			:: else
			num = num + 1;
		fi
	}
}

active [READERS] proctype rdr() {
	int local_counter[2*N];
	byte i;
	do
		::
		for(i in shared_counter) {
			local_counter[i] = shared_counter[i];
		}
		deduce_value:
		skip;
		d_step{
			for(i : 1 .. 2*N - 1) {
			assert (local_counter[i-1] <= local_counter[i]);
			}
			printf ("Read: ");
			for(i in local_counter) {
				printf("%d", local_counter[i]);
			}
			printf("\n");
		}
	od
}


active proctype wrtr() {
	int age = 0;
	byte i;
	do
		::
		inc_locally(age);
		for (i : 1 .. 2*N) {
			shared_counter[2*N - i] = age;
		}
	od
}
